\begin{tipo}{Trivia}
	\observador{keywords}{t: Trivia}{[Keyword]}
	\observador{preguntas}{t: Trivia}{[Pregunta]}
	\observador{participantes}{t: Trivia}{[Usuario]}
	\observador{ganadores}{t: Trivia}{[Usuario]}
	\observador{proxPregunta}{t: Trivia, u: Usuario}{Pregunta}
		\requiere{u \in participantes(t) \land u \notin ganadores(t)}
	\observador{puntajeAcumulado}{t: Trivia, u: Usuario}{Puntaje}
		\requiere{u \in participantes(t)}
		
	\medskip
	\invariante[noEsTrivialGanar]{\longitud{preguntas(t)} > 0}
	\invariante[noHayPreguntasRepetidas]{(\forall i, j \selec [0 .. | preguntas(t)|), i \neq j) \\ texto(preguntas(t)_i) \neq texto(preguntas(t)_j)}
	\invariante[noHayUsuariosRepetidas]{sinRepetidos(participantes(t) \land sinRepetidos(ganadores(t))}
	\invariante[proxPreguntaValida]{(\forall u \selec participantes(t), p \notin ganadores(t)) proxPregunta(t,u) \in preguntas(t)}
	\invariante[puntajesNoNegativos]{(\forall u \selec participantes(t)) puntajeAcumulado(t, u) \geq 0}
	\invariante[preguntasEntranEnSMS]{(\forall p \selec preguntas(t)) 0 < \longitud{texto(p)} \leq 139}
	\invariante[maximoPuntaje]{\sum{[ puntaje(p) | p \selec preguntas(t)]} \le 999}
	\invariante[losGanadoresSonParticipantes]{(\forall g \selec ganadores(t)) g \in participantes(t)}
	\invariante[keywordsSinEspacios]{(\forall k \selec keywords(t)) sinEspacios(k)}
\end{tipo}
